% embed_var(Emb, Var) :- Emb is a skolem var embedded in Var.
%
%
emb_var(_, Y) :-
	atomic(Y),
	!,
	fail.
emb_var(X, X) :-
	is_skolem(X).
emb_var(X, Y) :-
	functor(Y, F, N),
	emb_var(N, X, Y).

emb_var(N, X, Y) :-
		    (
		      ( N > 0, arg(N, Y, Arg),
	                emb_var(X, Arg)
		       );
		      ( N > 1, N1 is N-1,
		        emb_var(N1, X, Y)
		      )
		    ).

% X is a term inside Y
sub_term(X, X) :- !.
sub_term(X, Y) :-
	compound(Y),
	functor(Y, F, N),
	sub_term(N, X, Y).

sub_term(N, X, Y) :-
	N > 1,
	N1 is N-1,
	sub_term(N1, X, Y).
sub_term(N, X, Y) :-
	arg(N, Y, Arg),
	sub_term(X, Arg).



% egd(Body, V1, V2).
chase_egds :-
	egd(B, V1, V2),
	chase_egd_single(B, V1, V2),
	fail.
chase_egds.

%chase_egd(B, [], []).
%chase_egd(B, [X|Xs], [Y|Ys]) :- chase_egd_single(B, X, Y), chase_egd(B, Xs, Ys).

% chase egd for a single pair of variables
chase_egd_single(Body, V1, V2) :-
	call((Body, V1 \== V2)),
	collapse_var(V1,V2),
	setChanged.
chase_egd_single(_, _, _).

% setting flags for failing during collapsing varisables
set_chase_fail  :-
	assert(failDuringChasing).

unset_chase_fail :-
	retractall(failDuringChasing). 

last_chase_failed :-
    failDuringChasing.
    
% collapse_var(X, Y) :- collapse two variable/consts
% as in the consequence of chasing against egds.
collapse_var(X, X) :- !.

collapse_var(X, Y) :-
	constant(X),
	constant(Y),
	!,
	X \== Y,
	set_chase_fail,
	fail.
collapse_var(X, Y) :-
	is_skolem(X),
	constant(Y),
	!,
	sub_var(X, Y).
collapse_var(X, Y) :-
	constant(X),
	is_skolem(Y),
	!,
	sub_var(Y, X).
collapse_var(X, Y) :-
	is_skolem(X),
	is_skolem(Y),
	!,
	(preferred_skolem(X, Y) ->  sub_var(Y, X) ;  sub_var(X, Y)).


% sub_var(Old, New) :- replace every occurence of Old by New in all the facts.
sub_var(X, Y) :-
	var_fact(X, Fact),
	substitute(X, Y, Fact, NewFact),
	replace(Fact, NewFact),
	fail.
sub_var(_, _).

% replace(Old, New) :- replace an old fact by a new one and  update index.
replace(Old, New) :-
	removeFact(Old),
	addFact(New),
	!.

%
index_fact(Fact) :-
	compound(Fact),
	functor(Fact, _, N),
	index_fact(N, Fact).

index_fact(0, _) :- !.
index_fact(N, Fact) :-
	N > 0,
	!,
	arg(N, Fact, Arg),
	index_arg(Arg, Fact),
	N1 is N-1,
	index_fact(N1, Fact).

index_arg(Arg, Fact) :-
	emb_var(V, Arg),
	index(V, Fact),
	fail.
index_arg(_, _).

:- dynamic var_fact/2.
:- index(var_fact(1,1)).

index(Var, Fact) :- (
		      \+ var_fact(Var, Fact) ->
		       assert(var_fact(Var, Fact)) ;
		       true
		     ).
de_index(Fact) :-
	retractall(var_fact(_, Fact)).
de_index(Var, Fact) :-
	retractall(var_fact(Var, Fact)).

is_skolem(X) :-
	skolem_count(X, N).
skolem_count(X, N) :-
	functor(X, F, _),
	concat_atom([skolem, NAtom], '___', F),
	atom_number(NAtom, N).
smaller_skolem(X, Y) :-
	skolem_count(X, Nx),
	skolem_count(Y, Ny),
	(
	Nx < Ny;
	Nx = Ny,
	sizeOf(X, SizeX),
	sizeOf(Y, SizeY),
	SizeX < SizeY
	).

/* X is preferred to Y */
preferred_skolem(X, Y) :-
	( sub_term(X, Y) -> true ;
	   ( sub_term(Y, X) -> false ;
	   smaller_skolem(X, Y)
	   )
	).


sizeOf(Term, 1) :-
	atomic(Term), !.
sizeOf(Term, N) :-
	compound(Term),
	functor(Term, F, A),
	sizeOf(A, Term, NArgs, 0),
	N is NArgs + 1.
sizeOf(A, Term, N, C) :-
	A > 1, !,
	arg(A, Term, Arg),
	sizeOf(Arg, NArg),
	C1 is C+NArg,
	A1 is A-1,
	sizeOf(A1, Term, N, C1).
sizeOf(1, Term, N, C) :-
	arg(1, Term, Arg),
	sizeOf(Arg, NArg),
	N is C+NArg.




